|
In computer science, confluence is a property of rewriting systems, describing which terms in such a system can be rewritten in more than one way, to yield the same result. This article describes the properties in the most abstract setting of an abstract rewriting system. == Motivating examples == The usual rules of elementary arithmetic form an abstract rewriting system. For example, the expression (11 + 9) × (2 + 4) can be evaluated starting either at the left or at the right parentheses; however, in both cases the same result is obtained eventually. This suggests that the arithmetic rewriting system is a confluent one. A second, more abstract example is obtained from the following proof of each group element equalling the inverse of its inverse: 〔; here: p.134; axiom and proposition names follow the original text〕 This proof starts from the given group axioms A1-A3, and establishes five propositions R4, R6, R10, R11, and R12, each of them using some earlier ones, and R12 being the main theorem. Some of the proofs require non-obvious, if not creative, steps, like applying axiom A2 in reverse, thereby rewriting "1" to "''a''−1 ⋅ a" in the first step of R6's proof. One of the historical motivations to develop the ''theory of term rewriting'' was to avoid the need for such steps, which are difficult to find by an unexperienced human, let alone by a computer program. If a term rewriting system is confluent and ''terminating'', a straight-forward method exists to prove equality between two expressions (a.k.a. ''terms'') ''s'' and ''t'': Starting with ''s'', apply equalities〔then called ''rewrite rules'' to emphasize their left-to-right orientation〕 from left to right as long as possible, eventually obtaining a term ''s’''. Obtain from ''t'' a term ''t’'' in a similar way. If both terms ''s’'' and ''t’'' literally agree, then ''s'' and ''t'' are (not surprisingly) proven equal. More important, if they disagree, ''s'' and ''t'' cannot be equal. That is, any two terms ''s'' and ''t'' that can be proven equal at all, can be so by that method. The success of that method doesn't depend on a certain sophisticated order in which to apply rewrite rules, as confluence ensures that any sequence of rule applications will eventually lead to the same result (while the ''termination'' property ensures that any sequence will eventually reach an end at all). Therefore, if a confluent and terminating term rewriting system can be provided for some equational theory,〔The Knuth–Bendix completion algorithm can be used to compute such a system from a given set of equations. Such a system e.g. for groups is shown here, with its propositions consistently numbered. Using it, a proof of e.g. R6 consists in applying R11 and R12 in any order to (''a''−1)−1⋅1 to obtain ''a''.; no other rules are applicable.〕 not a tinge of creativity is required to perform proofs of term equality; that task hence becomes amenable to computer programs. Modern approaches handle more general ''abstract rewriting systems'' rather than ''term'' rewriting systems; the latter are a special case of the former. 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「Confluence (abstract rewriting)」の詳細全文を読む スポンサード リンク
|